Inference at * 1 1 
Iof proof for Lemma mul cancel in le:



1. a : 
2. b : 
3. n : 
4. (n * a)  (n * b)
5. ((n * a) < (n * b))  ((n * a) = (n * b))
  a  b 

latex

 by D 5 

latex

 1: 

 1: 5. (n * a) < (n * b)
 1:   a  b
 2: 

 2: 5. (n * a) = (n * b)
 2:   a  b
 .

Definitions

P  Q